X:Type, eq:EqDecider(X), f, g:x:X fp Type, x:X.
f || g  f(x)?Void  g(x)?Void  f(x)?Void = g(x)?Void  Type 

latex

Definitions	t  T, x:A. B(x), x. t(x), f || g, P  Q, a:A fp B(a), EqDecider(T), b, A, b, Prop, , f(x), Top, x  dom(f), P & Q, P  Q, Unit, f(x)?z
Lemmas	eqtt to assert, iff transitivity, eqff to assert, assert of bnot, bool wf, fpf-ap wf, fpf-dom wf, fpf-trivial-subtype-top, bnot wf, not wf, assert wf, deq wf, fpf wf, fpf-compatible wf